/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collections;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.ArrayCreation;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.VariableDeclaration;

import com.googlecode.syper.javasyp.formulae.Name;

/**
 * Keeps track of permissions for expressions and variables available in a given
 * code block.
 * A scope usually has a parent that holds permission info for expressions and
 * variables in the surrounding scope.
 * @author kevin
 */
public class Scope {

	/** Parent scope (for nested code blocks) */
	private final Scope parent;

	/** Code block this scope is associated with */
	private final ASTNode block;

	/** Receiver permission exposed inside this scope */
	private PermKind exposedReceiverPerm;

	/**
	 * Keys can be:
	 * <ul>
	 * <li>{@link Expression}s for permissions for intermediary expressions
	 * <li>{@link IVariableBinding}s for permissions for variables and fields
	 * <li>{@link ITypeBinding}s for receiver permissions
	 * </ul>
	 */
	private final Map<Object, PermInfo> perms =
		new LinkedHashMap<Object, PermInfo>();

	/** see {@link #perms} for allowed values */
	private final Set<Object> noPerms = new LinkedHashSet<Object>();

	/** Root scope (no parent, no block) */
	public Scope() {
		this(null, null);
	}

	/**
	 * Creates a scope object for the given code block with the given parent
	 * @param parent parent scope
	 * @param block code block managed by this scope
	 */
	public Scope(Scope parent, ASTNode block) {
		super();
		this.parent = parent;
		this.block = block;
	}

	/** copy constructor */
	public Scope(Scope s) {
		this(s.parent != null ? new Scope(s.parent) : null, s.block);
		this.exposedReceiverPerm = s.exposedReceiverPerm;
		this.noPerms.addAll(s.noPerms);
		for (Map.Entry<Object, PermInfo> p : s.perms.entrySet())
			this.perms.put(p.getKey(), new PermInfo(p.getValue()));
	}

	public Scope getParent() {
		return parent;
	}

	public ASTNode getBlock() {
		return block;
	}

	public void setExposedReceiver(PermKind p) {
		exposedReceiverPerm = p;
	}

	public PermKind getExposedReceiverPerm() {
		if (exposedReceiverPerm != null)
			return exposedReceiverPerm;
		else if (parent != null)
			return parent.getExposedReceiverPerm();
		else
			return null;
	}

	public boolean isReceiverAssignmentPermitted() {
		if (exposedReceiverPerm != null) {
			if (exposedReceiverPerm.isModifying())
				return true;
		}
		if (parent != null)
			return parent.isReceiverAssignmentPermitted();
		return false;
	}

	public PermKind getEffectiveReceiverPerm(ITypeBinding receiver) {
		PermInfo info = findInfo(receiver.getTypeDeclaration());
		return info == null ? null : info.getEffectivePerm();
	}

	public boolean isReceiverConsumable(ITypeBinding receiver) {
		PermInfo info = findInfo(receiver.getTypeDeclaration());
		return info == null ? true : info.isConsumable();
	}

	public RefType getEffectiveType(Expression e) {
		PermInfo info = getInfo(e);
		return info == null ? null : info.getEffectiveType();
	}

	public PermKind accessArrayElement(ArrayAccess e) {
		PermInfo info = getInfo(e.getArray());
		if (info == null)
			return null;
		PermInfo elementInfo = info.accessArrayElement(e);
		if (elementInfo == null)
			return noPerm(e);
		perms.put(e, elementInfo);
		return elementInfo.getEffectivePerm();
	}

	public void capture(Expression source, Expression target) {
		RefType t = getEffectiveType(source);
		if (t == null)
			return;
		try {
			consume(source, t.getPerm(), target, t.getElemDims());
			put(target, t);
			disable(source, target);
		} catch (PermissionException e) {
			throw new IllegalStateException("This should always succeed", e);
		}
	}

	/**
	 * Assigns the given source to the given target, releasing permissions previously
	 * assigned to the target if possible.
	 * @param source
	 * @param target
	 * @throws PermissionException
	 */
	public void assign(Expression source, Expression target)
	throws PermissionException {
		Object targetSelector = getSelector(target);
		PermInfo consumerInfo = findInfo(targetSelector);
		if (targetSelector instanceof IVariableBinding &&
				((IVariableBinding) targetSelector).isField() &&
				! isReceiverAssignmentPermitted()) {
			throw new PermissionException("Field assignment not permitted, need to expose Excl");
		} else if (targetSelector instanceof ArrayAccess) {
			Expression array = ((ArrayAccess) targetSelector).getArray();
			PermInfo arrayInfo = getInfo(array);
			PermKind arrayPerm;
			if (arrayInfo == null) {
				arrayPerm = null;
			} else {
				arrayPerm = arrayInfo.getConsumed(targetSelector);
				// if target hasn't consumed array perm see if array still has perm
				// (this will kick in if no perms declared for array dims)
				if (arrayPerm == null) {
					arrayPerm = arrayInfo.getEffectivePerm();
				} else {
					arrayInfo.release(arrayPerm, target);
					if (consumerInfo != null)
						consumerInfo.removeDisabled(array);
					// walk up nested array accesses and release
					while (array instanceof ArrayAccess) {
						Expression cell = array;
						PermInfo cellInfo = arrayInfo;
						array = ((ArrayAccess) array).getArray();
						arrayInfo = getInfo(array);
						if (arrayInfo != null) {
							PermKind p = arrayInfo.getConsumed(cell);
							if (p != null) {
								arrayInfo.release(p, cell);
								if (cellInfo != null)
									cellInfo.removeDisabled(array);
							}
						}
					}
				}
			}
			// do not use arrayInfo after this point as loop above may have changed it
			if (arrayPerm == null || ! arrayPerm.isModifying())
				throw new PermissionException((arrayPerm == null ? "No" : arrayPerm) +
						" array permission does not allow assigning its cells");
		} // else not a receiver field or array cell

		if (consumerInfo == null)
			// ignore, target doesn't have a permission
			return;

		if (targetSelector instanceof IVariableBinding) {
			PermInfo sourceInfo = getInfo(source);
			if (sourceInfo == null || consumerInfo.isConsumableBy(sourceInfo.getElemDims()))
				consumerInfo.addDisabled(source);

			// since we're re-assigning, get rid of previous consumers in this scope
			// ignore consumers from other scopes because assignment may not happen
			// on all paths on which permissions were consumed in surrounding outer scopes
			// TODO break / continue safety
			LinkedList<ASTNode> releasedConsumers = new LinkedList<ASTNode>();
			for (ASTNode c : consumerInfo.getConsumers()) {
				if (! secondFromInnerScope(target, c))
					continue;
				PermInfo oldConsumerInfo = getInfo(c);
				if (oldConsumerInfo != null)
					oldConsumerInfo.removeDisabled((IVariableBinding) targetSelector);
				releasedConsumers.add(c);
			}
			// release after iteration to avoid concurrent modification during iteration
			for (ASTNode c : releasedConsumers)
				consumerInfo.release(consumerInfo.getConsumed(c), c);
		} // else not a local or receiver field
		// disable source first so we can safely fail anywhere below

		// not sure if initial perm would work when exposing share
		consume(source, consumerInfo.getInitialPerm(), target,
				consumerInfo.getElemDims());
	}

	private static boolean secondFromInnerScope(final Expression n, final ASTNode c) {
		ASTNode s = n;
		while (! (s instanceof Statement))
			s = s.getParent();
		// find n's surrounding statement and use that stmt's parent as the scope
		s = s.getParent();

		ASTNode d = c;
		while (d != null) {
			if (d == s)
				return true;
			d = d.getParent();
		}
		return false;
	}

	// the following is supposed to release permissions bound by a variable
	// when that variable is reassigned
	// this doesn't currently work quite right in the presence of branches
	// where permissions assigned in one branch can be released in the other
	// so, we're going with the above, simpler version for now
	// that does not release when a variable is re-assigned
	// only when it goes out of scope it releases all sources

//	public void assign(Expression source, Expression target)
//	throws PermissionException {
//		Object targetSelector = getSelector(target);
//		PermInfo consumerInfo = findInfo(targetSelector);
//		if (consumerInfo == null)
//			// ignore, target doesn't have a permission
//			return;
//
//		// look up permission to be assigned to target
//		PermKind perm = consumerInfo.getInitialPerm();
//		if (targetSelector instanceof IVariableBinding) {
//			// assignment to local or receiver field...
//			if (consumerInfo.isConsumed()) {
//				// check if value being replaced is a problem
//				// this would trigger if borrowed parameters or locals
//				// are re-assigned when they're consumed
//				if (! consumerInfo.isConsumable())
//					// throwing here is not ideal since we miss
//					// the "consume" processing below
//					throw new PermissionException(
//							"Borrowed permission not returned for " + target);
//			} else if (! consumerInfo.getDisabled().isEmpty()) {
//				// release sources of previous value
//				// if there's multiple they come from conditional branches
//				// it's ok to release all since the variable is definitely re-assigned
//				// FIXME branches will look like subsequent assignments, problem?
//				IVariableBinding var = (IVariableBinding) targetSelector;
//				for (Expression e : consumerInfo.getDisabled()) {
//					PermInfo permInfo = getInfo(e);
//					if (permInfo != null)
//						permInfo.release(perm, var);
//				}
//				consumerInfo.getDisabled().clear();
//			}
//			// remember the source as being captured in the target
//			consumerInfo.addDisabled(source);
//		}
//		// finally, mark the source as consumed
//		// by doing this last consuming source can fail but we
//		// have the target updated correctly
//		consume(source, perm, target);
//	}

	public void consume(Expression e, RefType consumed, ASTNode node)
	throws PermissionException {
		consume(e, consumed.getPerm(), node, consumed.getElemDims());
	}

	private void consume(Expression e, PermKind consumed, ASTNode node,
			PermKind... elemDims)
	throws PermissionException {
		consume(e, consumed, node, Arrays.asList(elemDims));
	}

	private void consume(Expression e, PermKind consumed, ASTNode node,
			List<? extends PermKind> elemDims)
	throws PermissionException {
		PermInfo permInfo = getInfo(e);
		if (permInfo == null)
			throw new PermissionException("Need " + consumed + " but have no permission for " + e);

		permInfo.consume(consumed, node);
		if (! permInfo.isConsumableBy(elemDims))
			throw new PermissionException("Need dims " + elemDims +
					" but have " + permInfo.getElemDims());
	}

	public void consumeReceiver(ITypeBinding receiver, PermKind consumed, ASTNode consumer)
	throws PermissionException {
		PermInfo permInfo = findInfo(receiver);
		if (permInfo == null)
			throw new PermissionException("Need " + consumed + " but have no permission for receiver");
		permInfo.consume(consumed, consumer);
	}

	/**
	 * Release given permission consumed by {@code consumer} from {@code e}
	 * @param e
	 * @param consumed
	 * @param consumer
	 */
	public void release(Expression e, PermKind consumed, ASTNode consumer) {
		if (getInfo(consumer) != null && getInfo(consumer).isConsumed())
			throw new UnsupportedOperationException("Cannot release " + consumer + " for " + e + " because consumer is consumed itself");
		PermInfo permInfo = getInfo(e);
		if (permInfo == null)
			return; // keep going (should've caught this upon consume)...
//			throw new IllegalStateException("No information about " + e + " to release " + consumer);
		permInfo.release(consumed, consumer);
	}

	public void releaseReceiver(ITypeBinding receiver, PermKind consumed, ASTNode consumer) {
		if (getInfo(consumer) != null && getInfo(consumer).isConsumed())
			throw new UnsupportedOperationException("Cannot release " + consumer + " for receiver because consumer is consumed itself");
		PermInfo permInfo = findInfo(receiver);
		if (permInfo == null)
			return; // keep going (should've caught this upon consume)...
//			throw new IllegalStateException("No information about " + e + " to release " + consumer);
		permInfo.release(consumed, consumer);
	}

	/**
	 * <b>If the given node is a intermediary expression</b> and not
	 * a variable, release permissions disabled by the given node
	 * (unless expression's perm is consumable or is consumed itself)
	 * @param node
	 */
	public void releaseIfTemp(ASTNode node) {
		Expression key;
		try {
			Expression e = (Expression) node;
			if (e instanceof org.eclipse.jdt.core.dom.Name)
				// not a temp...
				return;
			key = (Expression) getSelector(e);
		} catch (ClassCastException e) {
			// variable or something like that
			return;
		}
		PermInfo info = findInfo(key);
		if (info != null && ! info.isConsumable() &&
				! info.isConsumed()) {
			releaseDisabled(info, key);
			// remove no-longer-needed temp for efficiency
			perms.remove(key);
		}
	}

	/**
	 * Returns permission info for the given AST node, if any.
	 * This is a convenience method for {@code findInfo(getSelector(node))}
	 * @param node any AST node for convenience; anything other than an expression will return {@code null}
	 * @return {@code null} if {@code node} is not an expression or has no permission info
	 */
	private PermInfo getInfo(ASTNode node) {
		if (node instanceof Expression)
			return findInfo(getSelector((Expression) node));
		else
			return null;
	}

	/**
	 * Returns a key for looking up permissions for the given expression in {@link #perms}.
	 * All bindings returned are normalized to their generic instance
	 * (using {@link IVariableBinding#getVariableDeclaration()} etc.)
	 * to simplify map lookups.
	 * @param e an expression
	 * @return The given expression or a normalized binding, see {@link #perms}:
	 * <ul>
	 * <li>a {@link IVariableBinding} if the expression represents a field or local
	 * <li>a {@link ITypeBinding} if the expression represents {@code this}
	 * <li>the expression itself otherwise (i.e., an intermediate or "temp" expression)
	 * </ul>
	 */
	private Object getSelector(Expression e) {
		Object selector;
		// TODO deal with non-receiver fields
		if (e instanceof SimpleName) {
			// local or receiver field
			selector = ((SimpleName) e).resolveBinding();
			if (! (selector instanceof IVariableBinding))
				throw new IllegalArgumentException("Not a variable or field: " + e);
			selector = ((IVariableBinding) selector).getVariableDeclaration();
		}
		else if (e instanceof FieldAccess && ((FieldAccess) e).getExpression() instanceof ThisExpression) {
			// this.f receiver field access
			selector = ((FieldAccess) e).resolveFieldBinding().getVariableDeclaration();
		}
		else if (e instanceof ThisExpression) {
			// use receiver type...
			selector = ((ThisExpression) e).resolveTypeBinding().getTypeDeclaration();
		}
		else {
			selector = e;
		}
		return selector;
	}

	/**
	 * Walks the scope stack to find info associated with given selector
	 * @param selector see {@link #perms}
	 * @return Permission info or <code>null</code> if not available
	 * @see #getSelector(Expression)
	 */
	private PermInfo findInfo(Object selector) {
		PermInfo localResult = perms.get(selector);
		if (localResult != null)
			return localResult;
		else if (parent != null)
			return parent.findInfo(selector);
		else
			return null;
	}

	/** Convenience for putting a consumable object permission, e.g. for a literal */
	public void put(Expression node, PermKind perm) {
		if (perm == null)
			// do nothing if there's no permission for this variable
			noPerm(node);
		else
			put(node, ObjectType.getInstance(perm, false, false));
	}

	/**
	 * Limited to array creation so we can check that there are dims.
	 * @param node
	 * @param type
	 */
	public void put(ArrayCreation node, RefType type) {
		if (type == null) {
			// do nothing if there's no permission
			noPerm(node);
			return;
		}
		if (type.getElemDims() == null || type.getElemDims().length != node.getType().getDimensions())
			throw new IllegalArgumentException("Need dimensions: " + node.getType().getDimensions());
		put((Expression) node, type);
	}

	/**
	 * Inject permission for expression, e.g., method call or {@code new}
	 * @param node
	 * @param type
	 */
	public void put(Expression node, RefType type) {
		if (type == null)
			// do nothing if there's no permission
			noPerm(node);
		else
			perms.put(node, createPermInfo(type));
	}

	/**
	 * Inject permission for local or method parameter
	 * @param node
	 * @param type
	 * @throws PermissionException
	 */
	public void put(VariableDeclaration node, RefType type) throws PermissionException {
		IVariableBinding selector = node.resolveBinding().getVariableDeclaration();
		if (selector.isField() || selector.isEnumConstant())
			throw new IllegalArgumentException("not a local: " + node);
		if (type == null) {
			// do nothing if there's no permission for this variable
			noPerm(selector);
			return;
		}
		perms.put(selector, createPermInfo(type));
		if (node.getInitializer() != null) {
			assign(node.getInitializer(), node.getName());
		}
	}

	/**
	 * Inject permission for field
	 * @param field
	 * @param type
	 */
	public void put(IVariableBinding field, RefType type) {
		if (! field.isField())
			throw new IllegalArgumentException("not a field: " + field);
		field = field.getVariableDeclaration();
		if (type == null) {
			// take out the field so it's not accessible
			perms.remove(field);
			noPerm(field);
		} else {
			perms.put(field, createPermInfo(type));
		}
	}

	public void putReceiver(ITypeBinding receiverType, RefType type) {
		if (type == null)
			// do nothing if there's no permission for this variable
			noPerm(receiverType);
		else
			perms.put(receiverType, createPermInfo(type));
	}

	private PermInfo createPermInfo(RefType type) {
		List<PermKind> dims;
		if (type.getElemDims() == null || type.getElemDims().length == 0) {
			dims = Collections.emptyList();
		} else {
			// make a copy just to be on the safe side
			dims = new ArrayList<PermKind>(type.getElemDims().length);
			for (PermKind d : type.getElemDims())
				dims.add(d);
			dims = Collections.unmodifiableList(dims);
		}
		return new PermInfo(type.getPerm(), type.isConsumed(), type.isReleased(), dims);
	}

	private PermKind noPerm(Object e) {
		e = e instanceof Expression ? getSelector((Expression) e) : e;
		noPerms.add(e);
		return null;
	}

	/**
	 * Checks and releases permissions for variables defined in this scope;
	 * fields will only be checked and not released
	 * @throws PermissionException if borrowed permissions are unavailable
	 */
	public void releaseScopeVariables() throws PermissionException {
		releaseScopeVariables(false);
	}

	/**
	 * Checks and releases permissions for variables defined in this scope;
	 * optionally releases borrowed fields
	 * @param releaseBorrowedFields set this to {@code true} for outermost
	 * scopes in constructors to check that constructor parameters declared
	 * as "released" are returned
	 * @throws PermissionException if borrowed permissions are unavailable
	 */
	public void releaseScopeVariables(boolean releaseBorrowedFields) throws PermissionException {
		// 1. release variables
		Map<IVariableBinding, PermInfo> fields = releaseBorrowedFields ?
				new LinkedHashMap<IVariableBinding, PermInfo>() : null;
		for (Map.Entry<Object, PermInfo> pair : perms.entrySet()) {
			final PermInfo info = pair.getValue();
			if (info.isConsumable())
				// only release borrowed variables...
				continue;

			final Object symbol = pair.getKey();

			// release local variables from disabled expressions
			// do this regardless of whether symbol was consumed
			// because it's *supposed to be* borrowed
			if (symbol instanceof IVariableBinding) {
				IVariableBinding var = (IVariableBinding) symbol;
				if (! var.isField()) {
					releaseDisabled(info, var);
				} else if (releaseBorrowedFields) {
					fields.put(var, info);
				}
			}

			// release array accesses from disabled expressions
			// do this regardless of whether symbol was consumed
			// because it's *supposed to be* borrowed
			if (symbol instanceof Expression) {
				releaseDisabled(info, symbol);
			}
		}

		// 2. check for errors
		String result = releaseErrors("Borrowed permission not returned for ", releaseBorrowedFields);
		if (result != null)
			throw new PermissionException(result);

		if (releaseBorrowedFields) {
			// 3. release fields (if desired)
			for (Map.Entry<IVariableBinding, PermInfo> f : fields.entrySet()) {
				releaseDisabled(f.getValue(), f.getKey());
			}

			// 4. check for errors
			result = releaseErrors("Permission not released for ", false);
			if (result != null)
				throw new PermissionException(result);
		}

	}

	private String releaseErrors(String msg, boolean skipReleasedWithFields) {
		StringBuilder result = null;
		// TODO produce separate errors that point to problematic variables
		for (Map.Entry<Object, PermInfo> pair : perms.entrySet()) {
			final PermInfo info = pair.getValue();
			if (info.isConsumable() ||
				(skipReleasedWithFields && info.isReleasedWithFields()))
				// only release borrowed variables...
				continue;

			final Object symbol = pair.getKey();
			if (info.isConsumed()) {
				// error condition! declared borrowed but consumed
				String obj;
				if (symbol instanceof IVariableBinding) {
					obj = ((IVariableBinding) symbol).getName();
				} else if (symbol instanceof ITypeBinding) {
					obj = "receiver";
				} else {
					obj = symbol.toString();
				}
				if (result == null)
					result = new StringBuilder();
				else
					result.append('\n');
				result.append(msg + obj);
			}
		}
		return result != null ? result.toString() : null;
	}

	/**
	 * Recursively releases permissions captured by the given consumer.
	 * @param info
	 * @param consumer
	 */
	private void releaseDisabled(final PermInfo info, Object consumer) {
		PermKind perm = info.getInitialPerm();
		for (Iterator<?> it = info.kill().iterator(); it.hasNext(); ) {
			Object e = it.next();
			// remove from disabled list so we don't release multiple times
			// from different root objects
			it.remove(); // remove immediately so we don't get into circles

			Object symbol;
			if (e instanceof Expression)
				symbol = getSelector((Expression) e);
			else
				symbol = e;
			PermInfo permInfo = findInfo(symbol);
			if (permInfo != null) {
				permInfo.release(perm, consumer);
				if (symbol instanceof Expression &&
						! permInfo.isConsumable() &&
						! permInfo.isConsumed()) {
					// recursively release
					releaseDisabled(permInfo, e);
					// TODO remove no-longer-needed temp for efficiency
//					perms.remove(symbol); causes CME but permInfo gets "kill"ed so it's ok
				}
			}
		}
	}

	/**
	 * Returns all locals and receiver fields with permissions and includes
	 * locals and fields without permissions (mapped to {@code null}) if
	 * parameter is {@code true}.
	 * @return
	 */
	public Map<IVariableBinding, PermKind> getLocalsAndReceiverFields(boolean includeNoPerms) {
		// TODO this is extremely inefficient....
		// could keep separate perms map just for IVariableBindings
		// could also keep result current when put is called
		Map<IVariableBinding, PermKind> result;
		if (parent == null)
			result = new LinkedHashMap<IVariableBinding, PermKind>();
		else
			result = parent.getLocalsAndReceiverFields(includeNoPerms);
		// do noPerms first in case we accidentally put something in that set
		for (Object o : noPerms) {
			if (o instanceof IVariableBinding) {
				if (includeNoPerms)
					result.put((IVariableBinding) o, null);
				else // override outer scope info
					result.remove(o);
			}
		}
		for (Map.Entry<Object, PermInfo> p : perms.entrySet()) {
			Object o = p.getKey();
			if (o instanceof IVariableBinding) {
				PermKind perm = p.getValue().getEffectivePerm();
				if (includeNoPerms || perm != null)
					result.put((IVariableBinding) o, perm);
				else // override outer scope info
					result.remove(o);
			}
		}
		return result;
	}

	public Map<Name, RefType> getRootsWithPermissions(AbstractHavocLookup<?> l) {
		// TODO this is extremely inefficient and kind of a hack in that it uses lookup
		// could also cache effective permission
		Map<Name, RefType> result;
		if (parent == null)
			result = new LinkedHashMap<Name, RefType>();
		else
			result = parent.getRootsWithPermissions(l);

		for (Object o : noPerms)
			// override anything from parent, probably unnecessary
			result.remove(getName(l, o));

		for (Map.Entry<Object, PermInfo> p : perms.entrySet()) {
			Name n = getName(l, p.getKey());
			RefType perm = p.getValue().getEffectiveType();
			if (perm == null)
				// override anything from parent, probably unnecessary
				result.remove(n);
			else
				result.put(n, perm);
		}
		return result;
	}

	private Name getName(AbstractHavocLookup<?> l, Object o) {
		if (o instanceof ITypeBinding)
			return l.getReceiver((ITypeBinding) o);
		if (o instanceof IVariableBinding) {
			IVariableBinding f = (IVariableBinding) o;
			if (f.isField())
				return l.getField(null /*receiver*/, f);
			else
				return l.getLocal(f);
		}
		return l.getName((Expression) o);
	}

	public void disable(Expression e, ASTNode node) {
		PermInfo permInfo = getInfo(node);
		if (permInfo == null)
			return; // keep going (should've caught this upon consume)...
		permInfo.addDisabled(e);
	}

	public void disableReceiver(ITypeBinding receiver, ASTNode node) {
		PermInfo permInfo = getInfo(node);
		if (permInfo == null)
			return; // keep going (should've caught this upon consume)...
		permInfo.addDisabledReceiver(receiver);
	}

	public void mergeIn(Scope other)
	throws PermissionException {
		this.releaseScopeVariables();
		other.releaseScopeVariables();
		join0(this.parent, other.parent);
	}

	private static void join0(Scope s1, Scope s2) {
		if (s1 == null & s2 == null)
			return;
		if (s1 == null | s2 == null)
			throw new IllegalStateException(
					"Different depths: " + s1 + " vs " + s2);
		if (s1.block != s2.block)
			throw new IllegalArgumentException(
					"Different scopes: " + s1.block + " vs " + s2.block);
		if (s1.exposedReceiverPerm != s2.exposedReceiverPerm)
			throw new IllegalStateException("Different exposure: " +
					s1.exposedReceiverPerm + " vs " + s2.exposedReceiverPerm);
		join0(s1.parent, s2.parent);
		if (s1.noPerms.retainAll(s2.noPerms))
			throw new IllegalStateException("Different no-perms");
		if (! s1.perms.keySet().equals(s2.perms.keySet()))
			throw new IllegalStateException("Different keys: " +
					s1.perms.keySet() + " vs " + s2.perms.keySet());
		for (Map.Entry<Object, PermInfo> p : s1.perms.entrySet()) {
			Object key = p.getKey();
			PermInfo pi1 = p.getValue();
			PermInfo pi2 = s2.perms.get(key);
			if (pi2 == null)
				throw new IllegalStateException("Missing: " + key);
			pi1.mergeIn(pi2);
		}
	}

	@Override
	public String toString() {
		StringBuilder result = new StringBuilder();
		result.append("Scope[").append(block).append(']');
		for (Map.Entry<Object, PermInfo> p : perms.entrySet()) {
			if (noPerms.contains(p.getKey()))
				continue;
			result.append('\n').append(p.getKey()).append(" --> ").append(p.getValue());
		}
		if (parent != null)
			result.append("\n\n").append(parent);
		return result.toString();
	}
}
